AXIOM EQ1
(∀ X) X=X 

AXIOM EQ2
(∀ X) (∀ Y) X=Y⊃Y=X 

AXIOM EQ3
(∀ X) (∀ Y) (∀ Z) X=Y∧Y=Z⊃X=Z 

AXIOM TABLEEMPTY
(∀ X) ¬X=ROBOT∧¬HOLDING(X,S0)⊃¬AT(X,TABLE,S0) 

AXIOM DIFFOBJ
¬BOX1=BOX2∧¬BOX1=TABLE∧¬BOX1=DOOR∧¬BOX1=OUTSIDE∧¬BOX2=TABLE∧¬BOX2=DOO~
R∧¬BOX2=OUTSIDE∧¬TABLE=DOOR∧¬TABLE=OUTSIDE∧¬DOOR=OUTSIDE 

AXIOM ATONE
(∀ X) (∀ P1) (∀ P2) (∀ S) AT(X,P1,S)∧AT(X,P2,S)⊃P1=P2 

AXIOM REDDOOR
(∃ X) RED X∧¬X=ROBOT∧AT(X,DOOR,S0)∧(∀ Y) AT(Y,DOOR,S0)∧¬Y=ROBOT∧¬HOLD~
ING(Y,S0)⊃RED Y 

AXIOM ISKEYBOX
KEYBOX=BOX1∨KEYBOX=BOX2 

AXIOM KEYBOX1
(∃ X) KEY X∧¬X=ROBOT∧AT(X,KEYBOX,S0)∧¬HOLDING(X,S0) 

AXIOM KEYBOX2
(∀ Y) AT(Y,KEYBOX,S0)∧¬Y=ROBOT∧¬HOLDING(Y,S0)⊃KEY Y 

AXIOM B1B2
¬BOX1=BOX2 

AXIOM B1T
¬BOX1=TABLE 

AXIOM B1D
¬BOX1=DOOR 

AXIOM B1O
¬BOX1=OUTSIDE 

AXIOM B2T
¬BOX2=TABLE 

AXIOM B2D
¬BOX2=DOOR 

AXIOM B2O
¬BOX2=OUTSIDE 

AXIOM TD
¬TABLE=DOOR 

AXIOM TO
¬TABLE=OUTSIDE 

AXIOM DO
¬DOOR=OUTSIDE 

AXIOM HOLDING
(∀ S) (∀ X) (∀ Y) AT(ROBOT,Y,S)∧HOLDING(X,S)⊃AT(X,Y,S) 

AXIOM HOLD2
(∀ S) (∀ X) (∀ Y) HOLDING(X,S)∧HOLDING(Y,S)⊃X=Y 

AXIOM PICKUP
(∀ S) ((λ SP) (∀ X) (∀ Y) AT(X,Y,S)≡AT(X,Y,SP)∧(∀ Z) AT(ROBOT,Z,S)∧(∃~
 X) ¬X=ROBOT∧AT(X,Z,S)⊃(∃ X) HOLDING(X,SP)) PICKUP S 

AXIOM GO1
(∀ S) (∀ Z) (∀ W) HOLDING(W,S)≡HOLDING(W,GOO(Z,S)) 

AXIOM GO2
(∀ S) (∀ Z) ¬Z=OUTSIDE∨(∃ X) AT(X,DOOR,S)∧KEY X⊃AT(ROBOT,Z,GOO(Z,S)) 

AXIOM GO3
(∀ S) (∀ Z) (∀ X) (∀ Y) AT(X,Y,S)∧¬X=ROBOT∧¬HOLDING(X,S)⊃AT(X,Y,GOO(Z~
,S)) 

AXIOM GO4
(∀ S) (∀ Y) (∀ X) ¬(AT(X,DOOR,S)∧KEY X)∧AT(ROBOT,Y,S)⊃AT(ROBOT,Y,GOO(~
OUTSIDE,S)) 

AXIOM GO5
(∀ S) (∀ Z) (∀ X) (∀ Y) ¬X=ROBOT∧¬HOLDING(X,S)∧AT(X,Y,GOO(Z,S))⊃AT(X,~
Y,S) 

AXIOM RELEASE1
(∀ S) (∀ X) (∀ Y) AT(X,Y,S)≡AT(X,Y,RELEASE S) 

AXIOM RELEASE2
(∀ S) (∀ X) ¬HOLDING(X,RELEASE S) 

AXIOM SITDEF
(∀ S) (∀ Y) (∀ X) XεSIT(Y,S)≡SITTING(X,Y,S) 

AXIOM SITSET
(∀ S) (∀ Y) ISSET SIT(Y,S) 

AXIOM EXTENSIONALITY
(∀ U) (∀ V) ISSET U∧ISSET V⊃(∀ X) XεU≡XεV⊃U=V 

AXIOM SITTING
(∀ S) (∀ X) (∀ Y) SITTING(X,Y,S)≡AT(X,Y,S)∧¬X=ROBOT∧¬HOLDING(X,S) 

PROOF ONE 

1:	XεSIT(Y,S)≡SITTING(X,Y,S) BY AXIOM(SITDEF,S,Y,X) 

2:	XεSIT(Y,GOO(Z,S))≡SITTING(X,Y,GOO(Z,S)) BY AXIOM(SITDEF,GOO(Z~
,S),Y,X) 

3:	SITTING(X,Y,S)≡AT(X,Y,S)∧¬X=ROBOT∧¬HOLDING(X,S) BY AXIOM(SITT~
ING,S,X,Y) 

4:	SITTING(X,Y,GOO(Z,S))≡AT(X,Y,GOO(Z,S))∧¬X=ROBOT∧¬HOLDING(X,GO~
O(Z,S)) BY AXIOM(SITTING,GOO(Z,S),X,Y) 

5:	HOLDING(X,S)≡HOLDING(X,GOO(Z,S)) BY AXIOM(GO1,S,Z,X) 

6:	AT(X,Y,S)∧¬X=ROBOT∧¬HOLDING(X,S)⊃AT(X,Y,GOO(Z,S)) BY AXIOM(GO~
3,S,Z,X,Y) 

7:	¬X=ROBOT∧¬HOLDING(X,S)∧AT(X,Y,GOO(Z,S))⊃AT(X,Y,S) BY AXIOM(GO~
5,S,Z,X,Y) 

8:	XεSIT(Y,S)≡XεSIT(Y,GOO(Z,S)) BY TAUT(XεSIT(Y,S)≡XεSIT(Y,GOO(Z~
,S)),1,2,3,4,5,6,7) 

9:	(∀ X) XεSIT(Y,S)≡XεSIT(Y,GOO(Z,S)) BY UG(8,X) 

10:	ISSET SIT(Y,S) BY AXIOM(SITSET,S,Y) 

11:	ISSET SIT(Y,GOO(Z,S)) BY AXIOM(SITSET,GOO(Z,S),Y) 

12:	ISSET SIT(Y,S)∧ISSET SIT(Y,GOO(Z,S))⊃(∀ X) XεSIT(Y,S)≡XεSIT(Y~
,GOO(Z,S))⊃SIT(Y,S)=SIT(Y,GOO(Z,S)) BY AXIOM(EXTENSIONALITY,SIT(Y,S),~
SIT(Y,GOO(Z,S))) 

13:	SIT(Y,S)=SIT(Y,GOO(Z,S)) BY TAUT(SIT(Y,S)=SIT(Y,GOO(Z,S)),9,1~
0,11,12) 

14:	(∀ Y) (∀ S) SIT(Y,S)=SIT(Y,GOO(Z,S)) BY UG(13,S,Y)